COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.R15:
C00013 00003	.ss(Computation,,)
C00020 ENDMK
C⊗;
.R15:

A term ?M is said to be in %3normal form%1 if it does not contain a redex as
a subterm.  If ?M#$c#?N and ?N is in normal form, then ?N is said to be a
%3normal form of ?M.  (Again, we may prefix ?β- and/or ?h- to these concepts
as appropriate.)

.group
Not all terms have a normal form.  Two such terms are:
.begin nofill; CENTER;

∪(λx.xx)(λx.xx)∩ and the %3paradoxical combinator%1:

∪Y%4λ%d ≡ λf.(λx.f(xx))(λx.f(xx))∩

.end
.apart
There are many possible "orders of evaluation" since a term, in general, may
contain more than one redex.  We would like to know how important the order of 
evaluation is (for example, can we get "different" normal forms from one ?λ-term
and are we guaranteed to find the right one, if it exists?).  Indeed, there
are ?λ-terms for which some sequences of reduction yield no normal form even
when the original term has a normal form.

.begin center;

For example, consider ∪(λw.z)((λx.xx)(λx.xx))
.end

which contains 2 ?β-redexes, the whole term and the argument ∪(λx.xx)(λx.xx)∩.  If
the outer redex is contracted, we immediately obtain the normal form ?z; but if
the argument is evaluated first, the reduction fails to terminate since
∪(λx.xx)(λx.xx)∩ repeatedly reduces to itself.⊗↓This is the "call-by-name"
vs. "call-by-value" distinction.←

The Church-Rosser Theorem assures us that any two reduction sequences which
terminate, will do so with the same result.

%7THEOREM 1%1 (Church-Rosser Theorem)####If ?X $c ?Y, there is a ?Z such that
?X#$r#?Z and ?Y#$r#?Z.   Diagrammatically:
.begin nofill;
			?X%41		          ?X%43  				?X%4n-1		


	∪X≡X%40			          ?X%42			      ?X%4n-2				?X%4n∪≡Y∩
					  	   									





					?Z
.end

The descending lines represent contractions, ascending lines represent abstractions
(reversed contractions); conversion between terms is a sequence of contractions
and/or abstractions, that is ?X#$c#?Y iff there is a sequence
.begin nofill;
		∪X≡?X0n≡Y∩ such that, for each i, 0≤i≤n-1, either
		?X%4i#$r#?X%4i+1%1  or  ?X%4i+1#$r#?X%4i%1.

.end
The solid lines in the diagram indicate the hypothesis of the theorem, the dashed
lines indicate the conclusion of the theorem.

%7Corollary 1.1%1  If ?M reduces to both ?X and ?Y, there is a ?Z such that
?X#$r#?Z and ?Y#$r#?Z.
.begin nofill; indent 0,10;
Proof:
.indent 10,10;fill;
If ?M reduces to ?X and ?M reduces to ?Y, then ?X#$c#?Y.  Thus we have a special case
of Theorem 1.
.end

%7 Corollary 1.2%1  If a term ?M has two normal forms ?X and ?Y, then ?X#?α-$c#?Y.
.begin nofill; indent 0,10;
Proof:
.indent 10,10;fill;
By corollary 1.1, there is a ?Z such that ?X#$r#?Z and ?Y#$r#?Z.  Since ?X is in
normal form, the only reduction applicable to ?X is ?α-conversion, hence
?X#?α-$c#?Z.  Similarly ?Y#?α-$c#?Z, so ?X#?α-$c#?Y by transitivity.
.end

Corollary 1.2 assures us that if a term has a normal form, it is unique up to a
change of its bound variables.  The Church-Rosser Theorem also establishes the
consistency of the ?λ-calculus, i.e., that not all sentences are provable.

%7Corollary 1.3%1  The ?λ-calculus is consistent.
.begin nofill; indent 0,10;
Proof:
.indent 10,10;fill;
Assume not, then ?M#$c#?N (that is ∪M=N∩ is a theorem) for all terms ?M and ?N.  In
particular, ∪λx.λy.x#$c#∪λx.λy.y∩.  Then ∪λx.λy.x∩ has two normal forms, itself
and ∪λx.λy.y∩, which are not ?α-convertible, which is a contradiction of
corollary 1.2.
.end

Now we would like to have a way to go about finding the normal form of a given 
term which will always terminate if the original term has a normal form.  If
at each stage in a reduction we reduce the leftmost redex in the term, we will
always achieve a normal form when one exists.  This is called %3normal order
reduction%1.  By the leftmost redex, we mean the one whose left-hand end
is furthest to the left.

.R13:
%7THEOREM 2%1  (Standardization theorem)####If a term ?X has a normal form,
then ?X reduces to normal form by normal order reduction.
.begin nofill;
For proof, see Wadsworth [15].
.end

.R14:
Remark:  The class %6N%1 of all terms in normal form can be defined inductively
by the following:
.begin nofill;
	1) ?zε%6N%1  (?z a variable)
	2) ?N0n ε%6N%1  => ?z?N%40?N%41%1...?N%4n%1ε%6N%1  (n≥0, ?z a variable)
	3) ?Nε%6N%1  =>  ∪(λx.N)∩ε%6N%1  (where ?N is not of the form ∪Mx∩ with ∪x≤FV(M)∩)
.end
All variables are terms and we get new terms by combination or abstraction.
Since we want only terms in normal form, an abstraction cannot appear as a rator in
a combination.  In other words, you can do any number of type 1)'s, then
any number of type 2)'s, but you cannot go back and forth between them.  Thus,
terms in normal form have the structure
.begin center;
∪λ?x1?x2...?xn∪.zN%41?N%42%1...?N%4m%1  n≥0, m≥0, ?z a variable,
where each ?N%4i%1 is in normal form, for 1≤i≤m.
.end


Some of the standard terms we will be using are:
.begin nofill; indent 30,30;
∪I ≡ λx.x
K ≡ λx.λy.x
B ≡ λf.λg.λx.f(gx)
.end
?I is of course interpreted as the identity function.  Note that a functional
application is a combination where the function is rator and the argument is 
rand.  Thus ∪IX=X∩ for any term ?X, but we do not get any kind of commutativity
for combinations, that is, ∪XI∩ is not, in general, equal to ?X.

?K is the function which, for an argument ?M, yields the constant function
∪λy.M∩, which has value ?M for all arguments ∪y∩.

The combinator ?B is connected with functional composition; for functions
∪f∩ and ∪g∩ we have
.begin center;
∪Bfg = λx.f(g(x)∩
.end
So ∪Bfg∩ represents ∪f∩⊗x∪g∩, the composition of ∪f∩ and ∪g∩.  If ?F is any term, we
write ?F%8n%1 for the composition of ?F with itself n times.  Note that ?F
"composed" with itself is %7not%1 ?F "combined" with itself.  We define ?F%8n%1
as follows:
.begin indent 30,30; nofill;
?F%80∪ ≡ I
?F%8n+1∪ ≡ F⊗x∪F%8n∪ ≡ BFF%8n
.end
Recall that our conventions for eliminating parentheses indicate that
∪F%8n+1 ∪≡ (BF)F%8n%1.  As an example of composition, consider the following
"powers" of ?K.
.begin nofill; indent 20,20;
?K%80∪ = I = λx.x
K%81∪ = BKI $r ∪K=λx.λy.x
K%82∪ = (BK)K $r ∪λx.λy.λz.x
K%83∪ = (BK)K%82 $r ∪λx.λy.λz.λw.x
  ...
K%8n∪ = (BK)K%8n-1 $r ∪λ?x1.?λ?x2....?λx%4n+1%d.x%41%1
.end
.R16:
Thus, ?K%8n%1 is a function of n+1 arguments which returns its first argument
as value.
.ss(Computation,,)
The Church-Rosser Theorem and a more recent result of B⊗ohm show that normal
forms are, in an appropriate sense, "separable" or "discretely 
distinguishable".

It seems natural to regard the reduction rules as rules of computation.
We can certainly describe an algorithm for computing normal forms; just use
normal order reduction. Computation would terminate precisely for those
terms which have a normal form. This would lead one to suppose that: 1)#terms
with normal forms should be distinguishable from those without, 2)#terms without
normal form are indistinguishable, and, 3)#that termination of programs is equivalent
to finding a normal form.

However this characterization of computation is inadequate. There are pairs of terms
which are equal in the models and yet, one will have a normal form while the other
does not. We shall also see that there are ways of distinguishing some terms although they
have no normal form. In fact, we shall see it would be inconsistent to equate all
terms not having a normal form.
  Consider the following example:
.begin indent 15,15; nofill;

∪M ≡ λx.x(λx.λy.x)(A) ≡ λx.x(K)(A)
N ≡ λx.x(λy.λx.x)(A) ≡ λx.x(KI)(A)
.end
where ?A is any term without a normal form, so that both ?M and ?N fail to have
 a normal form.  But ∪MK#β-$r#?K and ∪NK#β-$r#∪KI∩, so an identification of
?M and ?N would imply ∪K=KI∩, which would render the ?λ-calculus inconsistent
(as in the proof of corollary 1.3).  We exhibit the reductions of ∪MK∩ and
∪NK∩ to ?K and ∪KI∩ below.
.begin center;

∪MK ≡ (λx.x(λx.λy.x)(A))(λx.λy.x)

β-$r ∪(λx.λy.x)(λx.λy.x)(A)

$r ∪(λy%41∪.λx.λy.x)(A)

$r ∪λx.λy.x ≡ K


NK ≡ (λx.x(λy.λx.x)(A))(λx.λy.x)

β-$r ∪(λx.λy.x)(λy.λx.x)(A)

$r ∪(λy%41∪.λy.λx.x)(A)

$r ∪λy.λx.x $c ∪KI∩

.end

The concepts of solvability and head normal form are the beginnings of an attempt
to distinguish terms without normal forms.
To see how we can begin to draw distinctions between terms not having  normal
forms, we consider first the closed terms and how they behave when applied as
functions.
.begin tabit1(15)

Denote 
\⊗d ≡∪ λx.xx∩ and let 
\?M1∪ ≡ ⊗d⊗d and
\?M%42∪ ≡ ⊗d∪(λx.xxx)
.end

Neither of these terms has a normal form, and they are "hereditarily undefined"
in the sense that, no matter how they are applied as functions they never
yield normal forms as results. That is, for all integers k≥0, and all terms ?X1, ?X2, ...,
?X%4k%1, the applications ?M%4i%1?X1?X2...?X%4k%1 fail to have a normal form
for i= 1 or 2.

However, as we saw in the previous example, not all terms without normal forms
have this property.  This distinction is that of solvability.  A closed term
?M is said to be %3solvable%1 if there exist an integer k≥0 and terms ?X1, ?X2, ...,
?X%4k%1 such that ?M?X1?X2...?X%4k%1 has a normal form.  ?M is said to be
%3unsolvable%1 otherwise.

This definition has several immediate consequences and alternative 
statements.  First, a term having a normal form is always solvable (k=0);
more strongly, normal forms can be applied to suitable arguments to obtain any term
(not just a normal form) as result.

.R19:
%7LEMMA 3%1  If ?M is a (closed) term having a normal form ?N, and if ?X is any
term, then for some integer k≥0 and terms ?X1, ..., ?X%4k%1
.begin center;
∪M?X1?X2...?X%4k%d β-$r ?X
.end
.begin nofill;
Proof:
.end
.begin indent 10,10;
Recalling the structure of normal forms from the remark on {yon (R14)}, we
can write
.nofill;
		∪N ≡ λ?x1N∪.z?N1?N2...?N%4m%1
.fill;
with ∪z≡x%4i%1 for some i (since ?M, and thus ?N, is a closed term).
Now choose k=n, and for j = 1, 2, ..., k, define:
.nofill;
			?I, if j≠i
	  ?X%4j%d ≡%1
			?K%8m?X, if j=i
then,
.begin center;
∪(λ?x1N∪.z?N1?N%42%1...?N%4m)?X1N∪ ≡ (λ?x1...?xi...?xn∪.z?N1 ?N%42%d...N%4m%d)I...K%8m%dX...I
β-$r ∪K%8m%dX[#I...K%8m%dX...I/?x1?x2...?xi...?xn∪]?N1...?N%4m
.end
.fill
but ∪(K%8m%dX)?N1...?N%4m%1 ?β-$r ?X for %7any%1 terms ?N1...?N%4m%1, since
by previous remarks ({yon (R16)}) we know that ?K%8m%1 is a function of m+1
arguments which returns its first argument as value.⊗↓Note that we do not care
what the terms ?N1, ?N2, ..., ?N%4m%1 look like, in particular, they need not
be in normal form.←
.end